(declare-fun _substvar_47_ () Bool)
(declare-fun _substvar_53_ () Real)
(declare-fun v0 () Bool)
(declare-fun v4 () Bool)
(declare-fun r1 () Real)
(declare-fun r3 () Real)
(declare-fun r5 () Real)
(declare-fun r8 () Real)
(declare-fun v49 () Bool)
(assert (or (or v0 v4) v49 _substvar_47_))
(assert (or (= 0.0 r3 r8 (/ r1 r8) (+ 5.0 0.91 0.91 r5 71418009583.0) 0.91) v49 (= (/ 0.4 r1) r3 r8 0.0 _substvar_53_ 0.91)))
(check-sat)
